『［2021CAPE公開セミナー］ 論理学上級 Ⅱ-2「カリー・ハワード対応と『証明のデータ型としての命題』観」』
矢田部 俊介. [2021CAPE公開セミナー] 論理学上級 Ⅱ-2「カリー・ハワード対応と『証明のデータ型としての命題』観」 . 2021 https://www.youtube.com/watch?v=q02uYIc0s6g
証明のデータ型としての命題
直観主義論理において「命題を証明すること」と「計算すること」が同一視できる 意味の理論1.0
真理関数意味論
意味の理論2.0
命題の意味は(正規な)証明によって定まる
証明の(データ)型としての命題
証明は帰納的に構成される
証明を関数として解釈する
A→B
矛盾⊥
証明が存在しないため空集合
原始命題の証明
公理そのものを証明とみなす
$ a : A